These are archival webpages, generated on 2023-03-20 by Prove-It Beta Version 0.3, licensed under the GNU Public Licence by Sandia Corporation. See pyproveit.org for the lastest version.
logo
In [1]:
import proveit
from proveit import defaults, ExprTuple, ExprRange
from proveit import k, m, s, t, U
from proveit.numbers import (
    Mult, Exp, zero, one, two, subtract, exp2pi_i)
from proveit.linear_algebra import MatrixExp, TensorProd
from proveit.physics.quantum import var_ket_u, varphi
from proveit.physics.quantum.circuits import (
    QcircuitEquiv, phase_kickbacks_on_register)
from proveit.physics.quantum.QPE import (
    _s, _t, _ket_u, _U, _phase, _s_in_nat_pos, _u_ket_register, 
    _normalized_ket_u, _unitary_U, _phase_in_interval, _eigen_uu,
    QPE1_def, _psi_t_def, _psi_t_ket_is_normalized_vec)
theory = proveit.Theory() # the theorem's theory
In [2]:
%proving _psi_t_output
Under these presumptions, we begin our proof of
_psi_t_output:
(see dependencies)
In [3]:
_psi_t_output
In [4]:
defaults.assumptions = _psi_t_output.conditions
defaults.assumptions:
In [5]:
# don't combine factors of 2
Mult.change_simplification_directives(combine_all_exponents=False, 
                                      combine_numeric_rational_exponents=False) 
In [6]:
_psi_t_def
In [7]:
_psi_t = _psi_t_def.instantiate()
_psi_t:  ⊢  
In [8]:
_psi_t_ket_is_normalized_vec
In [9]:
_psi_t_ket_is_normalized_vec.instantiate()
In [10]:
target_circuit = _psi_t_output.instance_expr.lhs.operand
target_circuit:
In [11]:
QPE1_def
In [12]:
QPE1_inst = QPE1_def.instantiate({s:_s, U:_U})
QPE1_inst:  ⊢  
In [13]:
phase_kickbacks_on_register
In [14]:
Uexponentials = ExprTuple(ExprRange(k, MatrixExp(_U, Exp(two, k)), 
                                    subtract(t, one), zero, order='decreasing'))
Uexponentials:
In [15]:
phases = ExprTuple(ExprRange(k, Mult(Exp(two, k), _phase), 
                             subtract(t, one), zero, order='decreasing'))
phases:
In [16]:
kickbacks = phase_kickbacks_on_register.instantiate(
    {m:_s, U:Uexponentials, var_ket_u:_ket_u, varphi:phases})
kickbacks:  ⊢  
In [17]:
kickbacks_with_QPE1 = QPE1_inst.sub_left_side_into(
    kickbacks.inner_expr().lhs.operand)
kickbacks_with_QPE1:  ⊢  

For psi_t_tensor_u_expansion to simplify properly, we need to specify this default vector-space field, but we should be able to automate this in the future:

In [18]:
from proveit.numbers import Complex
from proveit.linear_algebra import VecSpaces
VecSpaces.default_field = Complex
VecSpaces.default_field:
In [19]:
psi_t_tensor_u__expansion = _psi_t.substitution(TensorProd(_psi_t.lhs, _ket_u))
psi_t_tensor_u__expansion:  ⊢  
In [20]:
output_consolidation = kickbacks_with_QPE1.lhs.operand.output_consolidation(
    replacements=[psi_t_tensor_u__expansion.derive_reversed()])
output_consolidation:  ⊢  
In [21]:
output_consolidation_from_desired = _psi_t_output.instance_expr.lhs.operand.output_consolidation()
output_consolidation_from_desired:  ⊢  
In [22]:
equiv = output_consolidation.apply_transitivity(output_consolidation_from_desired)
equiv:  ⊢  
In [23]:
equiv.sub_right_side_into(kickbacks_with_QPE1)
_psi_t_output may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".
In [24]:
%qed
proveit.physics.quantum.QPE._psi_t_output has been proven.
Out[24]:
 step typerequirementsstatement
0generalization1  ⊢  
1instantiation4, 2, 3  ⊢  
  : , : , :
2instantiation4, 5, 6  ⊢  
  : , : , :
3instantiation7, 8, 9  ⊢  
  : , : , :
4conjecture  ⊢  
 proveit.physics.quantum.circuits.rhs_prob_via_equiv
5instantiation10, 463, 751, 11, 12, 303, 13, 14, 15, 744, 746, 272, 16*  ⊢  
  : , : , : , : , :
6modus ponens17, 18  ⊢  
7conjecture  ⊢  
 proveit.physics.quantum.circuits.equiv_transitivity
8modus ponens19, 20  ⊢  
9instantiation31, 21  ⊢  
  : , :
10conjecture  ⊢  
 proveit.physics.quantum.circuits.phase_kickbacks_on_register
11instantiation601, 22, 651, 360  ⊢  
  : , : , : , :
12modus ponens23, 24  ⊢  
13axiom  ⊢  
 proveit.physics.quantum.QPE._normalized_ket_u
14instantiation601, 25, 651, 360  ⊢  
  : , : , : , :
15modus ponens26, 27  ⊢  
16instantiation688, 674, 736, 689, 28, 29, 690, 712, 693, 702, 703, 692,  ⊢  
  : , : , : , : , : , :
17instantiation47, 748, 469, 30  ⊢  
  : , : , : , : , : , : , : , :
18instantiation31, 32  ⊢  
  : , :
19instantiation47, 736, 748, 689, 48, 690  ⊢  
  : , : , : , : , : , : , : , :
20instantiation670, 33, 34  ⊢  
  : , : , :
21modus ponens35, 36  ⊢  
22instantiation670, 37, 416  ⊢  
  : , : , :
23instantiation418, 740, 741, 419  ⊢  
  : , : , : , :
24generalization38  ⊢  
25instantiation670, 39, 416  ⊢  
  : , : , :
26instantiation418, 740, 741, 419  ⊢  
  : , : , : , :
27generalization40  ⊢  
28instantiation694  ⊢  
  : , : , :
29instantiation704  ⊢  
  : , :
30instantiation601, 41, 651, 360  ⊢  
  : , : , : , :
31conjecture  ⊢  
 proveit.physics.quantum.circuits.equiv_reversal
32instantiation42, 463, 751, 59  ⊢  
  : , : , :
33instantiation670, 43, 44  ⊢  
  : , : , :
34instantiation238, 469, 67, 45, 46  ⊢  
  : , : , : , :
35instantiation47, 736, 748, 689, 48, 690  ⊢  
  : , : , : , : , : , : , : , :
36instantiation82, 654, 49, 751, 463, 50, 51, 303, 52, 53, 54, 55, 56, 270, 541, 689, 469, 96, 57, 553*  ⊢  
  : , : , : , : , : , :
37instantiation464, 465  ⊢  
  : , : , :
38instantiation58, 61, 358, 59,  ⊢  
  : , : , :
39instantiation464, 465  ⊢  
  : , : , :
40instantiation60, 61, 705, 62,  ⊢  
  : , : , : , :
41instantiation670, 63, 416  ⊢  
  : , : , :
42axiom  ⊢  
 proveit.physics.quantum.QPE.QPE1_def
43instantiation670, 64, 65  ⊢  
  : , : , :
44instantiation238, 469, 66, 67, 68  ⊢  
  : , : , : , :
45instantiation69, 469  ⊢  
  : , :
46instantiation393, 743, 327, 328, 329, 330*  ⊢  
  : , : , : , : , : , :
47conjecture  ⊢  
 proveit.physics.quantum.circuits.circuit_equiv_temporal_sub
48instantiation704  ⊢  
  : , :
49instantiation704  ⊢  
  : , :
50instantiation704  ⊢  
  : , :
51instantiation70, 71  ⊢  
  : , :
52instantiation601, 72, 73, 74  ⊢  
  : , : , : , :
53instantiation611, 75  ⊢  
  : , :
54instantiation704  ⊢  
  : , :
55instantiation611, 76  ⊢  
  : , :
56instantiation601, 77, 577, 78  ⊢  
  : , : , : , :
57instantiation181, 674, 79, 184, 80, 186  ⊢  
  : , :
58conjecture  ⊢  
 proveit.linear_algebra.matrices.exponentiation.U_closure
59axiom  ⊢  
 proveit.physics.quantum.QPE._unitary_U
60conjecture  ⊢  
 proveit.linear_algebra.matrices.exponentiation.unital2pi_eigen_exp_application
61instantiation413, 736, 81,  ⊢  
  : , :
62axiom  ⊢  
 proveit.physics.quantum.QPE._eigen_uu
63instantiation464, 465  ⊢  
  : , : , :
64instantiation82, 431, 83, 652, 84, 463, 85, 86, 87, 303, 88, 89, 90, 91, 92, 93, 94, 270, 169, 689, 95, 96, 97, 553, 98, 99*, 100*, 101*  ⊢  
  : , : , : , : , : , :
65instantiation238, 469, 102, 103, 104  ⊢  
  : , : , : , :
66instantiation601, 105, 651, 360  ⊢  
  : , : , : , :
67instantiation601, 106, 651, 360  ⊢  
  : , : , : , :
68instantiation293, 294, 295, 441*  ⊢  
  : , : , : , :
69conjecture  ⊢  
 proveit.core_expr_types.tuples.range_from1_len_typical_eq
70theorem  ⊢  
 proveit.logic.booleans.conjunction.left_from_and
71instantiation107, 751  ⊢  
  :
72instantiation108  ⊢  
  : , : , :
73instantiation669  ⊢  
  :
74instantiation611, 109  ⊢  
  : , :
75instantiation214, 110, 553  ⊢  
  : , : , :
76instantiation268, 110, 541  ⊢  
  : , : , :
77instantiation111  ⊢  
  : , :
78instantiation611, 112  ⊢  
  : , :
79instantiation694  ⊢  
  : , : , :
80instantiation611, 443  ⊢  
  : , :
81instantiation548, 113,  ⊢  
  :
82conjecture  ⊢  
 proveit.physics.quantum.circuits.output_consolidation
83instantiation601, 114, 130, 125  ⊢  
  : , : , : , :
84instantiation357, 730, 741, 652, 289  ⊢  
  : , : , :
85instantiation601, 115, 130, 125  ⊢  
  : , : , : , :
86instantiation409, 116, 208  ⊢  
  : , : , :
87modus ponens117, 118  ⊢  
88instantiation601, 119, 120, 121  ⊢  
  : , : , : , :
89instantiation611, 122  ⊢  
  : , :
90instantiation611, 123  ⊢  
  : , :
91instantiation601, 124, 130, 125  ⊢  
  : , : , : , :
92instantiation611, 126  ⊢  
  : , :
93instantiation657, 127, 128  ⊢  
  : , : , :
94instantiation601, 129, 130, 131  ⊢  
  : , : , : , :
95modus ponens132, 133  ⊢  
96instantiation388, 469, 414  ⊢  
  : , :
97instantiation134, 736, 384, 748, 135, 530, 136, 137  ⊢  
  : , : , : , : , : , :
98instantiation657, 138, 139,  ⊢  
  : , : , :
99instantiation657, 140, 141  ⊢  
  : , : , :
100instantiation657, 142, 143  ⊢  
  : , : , :
101instantiation657, 144, 145,  ⊢  
  : , : , :
102instantiation601, 146, 651, 360  ⊢  
  : , : , : , :
103instantiation601, 147, 651, 360  ⊢  
  : , : , : , :
104instantiation293, 294, 295  ⊢  
  : , : , : , :
105instantiation350, 654, 148, 352, 353, 354, 384, 355*  ⊢  
  : , : , : , :
106instantiation670, 149, 416  ⊢  
  : , : , :
107conjecture  ⊢  
 proveit.physics.quantum.QPE._psi_t_ket_is_normalized_vec
108conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3
109instantiation670, 150, 151  ⊢  
  : , : , :
110instantiation388, 736, 379  ⊢  
  : , :
111conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2
112instantiation670, 152, 153  ⊢  
  : , : , :
113instantiation587, 735, 154,  ⊢  
  :
114instantiation350, 172, 155, 174, 175, 354, 384, 176*  ⊢  
  : , : , : , :
115instantiation350, 172, 156, 174, 175, 354, 384, 176*  ⊢  
  : , : , : , :
116instantiation409, 157, 158  ⊢  
  : , : , :
117instantiation418, 730, 741, 289  ⊢  
  : , : , : , :
118generalization159  ⊢  
119instantiation350, 172, 160, 161, 175, 354, 465, 162*  ⊢  
  : , : , : , :
120instantiation681, 712, 662  ⊢  
  : , :
121instantiation611, 163  ⊢  
  : , :
122instantiation214, 168, 553  ⊢  
  : , : , :
123instantiation238, 469, 221, 164, 165  ⊢  
  : , : , : , :
124instantiation350, 172, 166, 174, 175, 354, 384, 176*  ⊢  
  : , : , : , :
125instantiation611, 167  ⊢  
  : , :
126instantiation268, 168, 169  ⊢  
  : , : , :
127instantiation611, 170  ⊢  
  : , :
128instantiation611, 171  ⊢  
  : , :
129instantiation350, 172, 173, 174, 175, 354, 384, 176*  ⊢  
  : , : , : , :
130instantiation669  ⊢  
  :
131instantiation611, 177  ⊢  
  : , :
132instantiation418, 740, 741, 419  ⊢  
  : , : , : , :
133generalization178  ⊢  
134conjecture  ⊢  
 proveit.logic.booleans.conjunction.disassociate
135instantiation704  ⊢  
  : , :
136instantiation601, 179, 484, 180  ⊢  
  : , : , : , :
137instantiation181, 182, 183, 184, 515, 185, 186  ⊢  
  : , :
138instantiation599, 187,  ⊢  
  : , : , :
139instantiation657, 188, 189,  ⊢  
  : , : , :
140instantiation599, 190  ⊢  
  : , : , :
141instantiation611, 191  ⊢  
  : , :
142instantiation599, 192  ⊢  
  : , : , :
143instantiation194, 652  ⊢  
  : , :
144instantiation599, 193,  ⊢  
  : , : , :
145instantiation194, 195,  ⊢  
  : , :
146instantiation350, 654, 196, 352, 353, 354, 384, 355*  ⊢  
  : , : , : , :
147instantiation670, 197, 416  ⊢  
  : , : , :
148instantiation704  ⊢  
  : , :
149instantiation464, 465  ⊢  
  : , : , :
150instantiation464, 198  ⊢  
  : , : , :
151instantiation657, 199, 200  ⊢  
  : , : , :
152instantiation464, 201  ⊢  
  : , : , :
153instantiation657, 202, 203  ⊢  
  : , : , :
154instantiation204, 740, 741, 738,  ⊢  
  : , : , :
155instantiation694  ⊢  
  : , : , :
156instantiation694  ⊢  
  : , : , :
157instantiation557, 558, 472, 205  ⊢  
  : , : , : , :
158instantiation599, 206  ⊢  
  : , : , :
159instantiation409, 207, 208,  ⊢  
  : , : , :
160instantiation694  ⊢  
  : , : , :
161instantiation694  ⊢  
  : , : , :
162instantiation657, 209, 210  ⊢  
  : , : , :
163instantiation670, 211, 212  ⊢  
  : , : , :
164instantiation601, 213, 651, 360  ⊢  
  : , : , : , :
165instantiation214, 294, 400, 441*  ⊢  
  : , : , :
166instantiation694  ⊢  
  : , : , :
167instantiation468, 378  ⊢  
  : , :
168instantiation444, 215, 216  ⊢  
  :
169instantiation657, 217, 218  ⊢  
  : , : , :
170instantiation238, 469, 222, 219, 220  ⊢  
  : , : , : , :
171instantiation238, 469, 221, 222, 223  ⊢  
  : , : , : , :
172conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat3
173instantiation694  ⊢  
  : , : , :
174instantiation694  ⊢  
  : , : , :
175instantiation694  ⊢  
  : , : , :
176instantiation657, 224, 225  ⊢  
  : , : , :
177instantiation670, 226, 227  ⊢  
  : , : , :
178instantiation444, 228, 229,  ⊢  
  :
179instantiation670, 230, 530  ⊢  
  : , : , :
180instantiation611, 231  ⊢  
  : , :
181conjecture  ⊢  
 proveit.logic.booleans.conjunction.and_if_all
182conjecture  ⊢  
 proveit.numbers.numerals.decimals.nat4
183instantiation232  ⊢  
  : , : , : , :
184instantiation669  ⊢  
  :
185modus ponens233, 234  ⊢  
186instantiation669  ⊢  
  :
187instantiation605, 748, 689, 690, 237, 646, 662,  ⊢  
  : , : , : , : , : , : , :
188instantiation643, 689, 674, 748, 690, 235, 237, 662, 646, 682,  ⊢  
  : , : , : , : , : , :
189instantiation614, 736, 689, 236, 690, 237, 662, 682,  ⊢  
  : , : , : , : , : , : , : , :
190instantiation238, 469, 239, 301, 240  ⊢  
  : , : , : , :
191instantiation599, 241, 242*  ⊢  
  : , : , :
192instantiation599, 553  ⊢  
  : , : , :
193instantiation599, 348,  ⊢  
  : , : , :
194conjecture  ⊢  
 proveit.physics.quantum.circuits.unary_multi_output_reduction
195instantiation243, 244, 245,  ⊢  
  :
196instantiation704  ⊢  
  : , :
197instantiation464, 465  ⊢  
  : , : , :
198instantiation505, 674, 246, 736, 379, 748  ⊢  
  : , :
199instantiation599, 483  ⊢  
  : , : , :
200instantiation637, 689, 736, 748, 690, 247, 712, 634, 682, 248*  ⊢  
  : , : , : , : , : , :
201instantiation505, 674, 249, 748, 379  ⊢  
  : , :
202instantiation599, 483  ⊢  
  : , : , :
203instantiation637, 689, 736, 748, 690, 353, 682, 634, 250*  ⊢  
  : , : , : , : , : , :
204conjecture  ⊢  
 proveit.numbers.number_sets.integers.interval_upper_bound
205instantiation519, 558, 520, 251  ⊢  
  : , : , : , :
206instantiation599, 252  ⊢  
  : , : , :
207instantiation557, 558, 472, 253,  ⊢  
  : , : , : , :
208instantiation599, 254  ⊢  
  : , : , :
209instantiation457, 674, 255, 256, 460, 416  ⊢  
  : , : , : , :
210instantiation657, 257, 258  ⊢  
  : , : , :
211instantiation464, 259  ⊢  
  : , : , :
212instantiation657, 260, 261  ⊢  
  : , : , :
213instantiation350, 654, 262, 352, 353, 354, 384, 355*  ⊢  
  : , : , : , :
214conjecture  ⊢  
 proveit.core_expr_types.tuples.partition_front
215instantiation742, 263, 264  ⊢  
  : , :
216instantiation496, 265  ⊢  
  : , :
217instantiation643, 689, 736, 748, 690, 381, 662, 682, 646  ⊢  
  : , : , : , : , : , :
218instantiation266, 682, 662, 617  ⊢  
  : , : , :
219instantiation601, 267, 651, 360  ⊢  
  : , : , : , :
220instantiation268, 269, 270, 271*  ⊢  
  : , : , :
221instantiation599, 272  ⊢  
  : , : , :
222instantiation599, 273  ⊢  
  : , : , :
223instantiation393, 710, 327, 274, 275, 276*  ⊢  
  : , : , : , : , : , :
224instantiation457, 674, 277, 278, 460, 530  ⊢  
  : , : , : , :
225instantiation657, 279, 280  ⊢  
  : , : , :
226instantiation464, 281  ⊢  
  : , : , :
227instantiation657, 282, 283  ⊢  
  : , : , :
228instantiation742, 735, 746,  ⊢  
  : , :
229instantiation620, 666, 542, 284, 285, 286*, 287*,  ⊢  
  : , : , :
230instantiation464, 384  ⊢  
  : , : , :
231instantiation468, 288  ⊢  
  : , :
232conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
233instantiation418, 730, 741, 289  ⊢  
  : , : , : , :
234generalization290  ⊢  
235instantiation694  ⊢  
  : , : , :
236instantiation704  ⊢  
  : , :
237instantiation749, 728, 291,  ⊢  
  : , : , :
238conjecture  ⊢  
 proveit.core_expr_types.operations.operands_substitution_via_tuple
239instantiation601, 292, 651, 360  ⊢  
  : , : , : , :
240instantiation293, 294, 295  ⊢  
  : , : , : , :
241instantiation296, 751  ⊢  
  :
242instantiation297, 689, 465, 748, 690, 416, 298, 299, 300, 301, 302, 303  ⊢  
  : , : , : , : , : , : , : , : , : , :
243conjecture  ⊢  
 proveit.numbers.number_sets.integers.pos_int_is_natural_pos
244instantiation742, 720, 746,  ⊢  
  : , :
245instantiation304, 475, 640, 305, 306, 307*, 308*,  ⊢  
  : , : , :
246instantiation694  ⊢  
  : , : , :
247instantiation704  ⊢  
  : , :
248instantiation657, 309, 310  ⊢  
  : , : , :
249instantiation694  ⊢  
  : , : , :
250instantiation657, 311, 680  ⊢  
  : , : , :
251instantiation557, 558, 312, 560  ⊢  
  : , : , : , :
252instantiation599, 313  ⊢  
  : , : , :
253instantiation519, 558, 520, 314,  ⊢  
  : , : , : , :
254instantiation315, 712  ⊢  
  :
255instantiation694  ⊢  
  : , : , :
256instantiation694  ⊢  
  : , : , :
257instantiation605, 748, 689, 690, 682, 662  ⊢  
  : , : , : , : , : , : , :
258instantiation637, 689, 736, 748, 690, 606, 682, 662, 680*  ⊢  
  : , : , : , : , : , :
259instantiation749, 511, 316  ⊢  
  : , : , :
260instantiation599, 483  ⊢  
  : , : , :
261instantiation601, 317, 318, 319  ⊢  
  : , : , : , :
262instantiation704  ⊢  
  : , :
263instantiation749, 750, 431  ⊢  
  : , : , :
264instantiation696, 320, 433  ⊢  
  : , : , :
265instantiation572, 321  ⊢  
  : , :
266conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_23
267instantiation322, 323, 324*  ⊢  
  : , : , : , :
268conjecture  ⊢  
 proveit.core_expr_types.tuples.partition_back
269instantiation444, 325, 326  ⊢  
  :
270instantiation581, 634, 682, 553  ⊢  
  : , : , :
271instantiation641, 682, 662, 617  ⊢  
  : , : , :
272instantiation393, 743, 327, 328, 329, 330*  ⊢  
  : , : , : , : , : , :
273instantiation657, 331, 332  ⊢  
  : , : , :
274instantiation611, 333  ⊢  
  : , :
275instantiation611, 334  ⊢  
  : , :
276instantiation643, 689, 736, 748, 690, 335, 336, 646, 662,  ⊢  
  : , : , : , : , : , :
277instantiation694  ⊢  
  : , : , :
278instantiation694  ⊢  
  : , : , :
279instantiation643, 748, 736, 645, 682, 662, 646  ⊢  
  : , : , : , : , : , :
280instantiation615, 689, 748, 690, 682, 662, 617  ⊢  
  : , : , : , : , : , : , : , :
281instantiation505, 674, 337, 469, 379, 748  ⊢  
  : , :
282instantiation599, 483  ⊢  
  : , : , :
283instantiation635, 748, 662, 682  ⊢  
  : , : , : , :
284instantiation522, 729, 716,  ⊢  
  : , :
285instantiation338, 542, 729, 716, 339, 340,  ⊢  
  : , : , :
286instantiation601, 341, 342, 343  ⊢  
  : , : , : , :
287instantiation601, 344, 345, 346,  ⊢  
  : , : , : , :
288instantiation444, 698, 347  ⊢  
  :
289instantiation620, 542, 716, 678, 621, 438*, 471*  ⊢  
  : , : , :
290instantiation611, 348,  ⊢  
  : , :
291instantiation749, 731, 349,  ⊢  
  : , : , :
292instantiation350, 654, 351, 352, 353, 354, 384, 355*  ⊢  
  : , : , : , :
293conjecture  ⊢  
 proveit.core_expr_types.tuples.merge_front
294instantiation388, 689, 507  ⊢  
  : , :
295instantiation611, 400  ⊢  
  : , :
296axiom  ⊢  
 proveit.physics.quantum.QPE._psi_t_def
297conjecture  ⊢  
 proveit.linear_algebra.tensors.tensor_prod_disassociation
298instantiation601, 356, 651, 360  ⊢  
  : , : , : , :
299instantiation357, 740, 741, 558, 419  ⊢  
  : , : , :
300instantiation594, 358  ⊢  
  :
301instantiation601, 359, 651, 360  ⊢  
  : , : , : , :
302modus ponens361, 362  ⊢  
303axiom  ⊢  
 proveit.physics.quantum.QPE._u_ket_register
304conjecture  ⊢  
 proveit.numbers.addition.strong_bound_via_left_term_bound
305instantiation522, 695, 721,  ⊢  
  : , :
306instantiation363, 640, 695, 721, 364, 365,  ⊢  
  : , : , :
307instantiation601, 366, 367, 368  ⊢  
  : , : , : , :
308instantiation601, 369, 370, 371,  ⊢  
  : , : , : , :
309instantiation599, 372  ⊢  
  : , : , :
310conjecture  ⊢  
 proveit.numbers.numerals.decimals.add_2_1
311instantiation599, 373  ⊢  
  : , : , :
312instantiation711, 595, 374  ⊢  
  : , :
313instantiation599, 375  ⊢  
  : , : , :
314instantiation557, 558, 376, 560,  ⊢  
  : , : , : , :
315conjecture  ⊢  
 proveit.numbers.exponentiation.complex_x_to_first_power_is_x
316instantiation490, 736, 689, 377, 690, 378, 379, 748, 491  ⊢  
  : , : , : , : , :
317instantiation643, 689, 736, 690, 381, 380, 662, 682, 634  ⊢  
  : , : , : , : , : , :
318instantiation635, 736, 748, 381, 662, 682  ⊢  
  : , : , : , :
319instantiation637, 748, 736, 689, 606, 690, 662, 682, 680*  ⊢  
  : , : , : , : , : , :
320instantiation708, 382  ⊢  
  : , :
321instantiation608, 431  ⊢  
  :
322conjecture  ⊢  
 proveit.core_expr_types.tuples.extended_range_len
323instantiation383, 384  ⊢  
  : , : , :
324instantiation657, 385, 386  ⊢  
  : , : , :
325instantiation742, 744, 495  ⊢  
  : , :
326instantiation496, 387  ⊢  
  : , :
327instantiation388, 389, 507  ⊢  
  : , :
328instantiation611, 390  ⊢  
  : , :
329instantiation611, 391  ⊢  
  : , :
330instantiation657, 392, 586,  ⊢  
  : , : , :
331instantiation393, 740, 394, 395, 396  ⊢  
  : , : , : , : , : , :
332modus ponens397, 398  ⊢  
333instantiation657, 399, 400  ⊢  
  : , : , :
334instantiation657, 401, 553  ⊢  
  : , : , :
335instantiation704  ⊢  
  : , :
336instantiation749, 728, 402,  ⊢  
  : , : , :
337instantiation694  ⊢  
  : , : , :
338conjecture  ⊢  
 proveit.numbers.ordering.less_eq_add_right
339instantiation421, 740, 741, 738,  ⊢  
  : , : , :
340instantiation403, 748  ⊢  
  :
341instantiation643, 689, 736, 748, 690, 589, 649, 682, 642  ⊢  
  : , : , : , : , : , :
342instantiation643, 736, 689, 589, 645, 690, 649, 682, 662, 646  ⊢  
  : , : , : , : , : , :
343instantiation657, 404, 423  ⊢  
  : , : , :
344instantiation643, 689, 736, 748, 690, 405, 723, 682, 642,  ⊢  
  : , : , : , : , : , :
345instantiation643, 736, 689, 405, 645, 690, 723, 682, 662, 646,  ⊢  
  : , : , : , : , : , :
346instantiation615, 748, 689, 690, 723, 682, 662, 617,  ⊢  
  : , : , : , : , : , : , : , :
347instantiation496, 621  ⊢  
  : , :
348instantiation657, 406, 407,  ⊢  
  : , : , :
349instantiation749, 734, 408,  ⊢  
  : , : , :
350conjecture  ⊢  
 proveit.core_expr_types.tuples.general_len
351instantiation704  ⊢  
  : , :
352instantiation704  ⊢  
  : , :
353instantiation704  ⊢  
  : , :
354instantiation409, 748, 460  ⊢  
  : , : , :
355instantiation657, 410, 411  ⊢  
  : , : , :
356instantiation670, 412, 416  ⊢  
  : , : , :
357conjecture  ⊢  
 proveit.logic.booleans.conjunction.redundant_conjunction_general
358instantiation413, 736, 414  ⊢  
  : , :
359instantiation670, 415, 416  ⊢  
  : , : , :
360instantiation611, 417  ⊢  
  : , :
361instantiation418, 740, 741, 419  ⊢  
  : , : , : , :
362generalization420  ⊢  
363conjecture  ⊢  
 proveit.numbers.ordering.less_eq_add_right_strong
364instantiation421, 730, 741, 726,  ⊢  
  : , : , :
365instantiation608, 654  ⊢  
  :
366instantiation643, 689, 736, 748, 690, 644, 649, 712, 424  ⊢  
  : , : , : , : , : , :
367instantiation643, 736, 689, 644, 633, 690, 649, 712, 662, 683  ⊢  
  : , : , : , : , : , :
368instantiation657, 422, 423  ⊢  
  : , : , :
369instantiation643, 689, 736, 748, 690, 425, 677, 712, 424,  ⊢  
  : , : , : , : , : , :
370instantiation643, 736, 689, 425, 633, 690, 677, 712, 662, 683,  ⊢  
  : , : , : , : , : , :
371instantiation615, 748, 689, 690, 677, 712, 662, 577,  ⊢  
  : , : , : , : , : , : , : , :
372instantiation426, 712  ⊢  
  :
373instantiation426, 682  ⊢  
  :
374instantiation670, 427, 428  ⊢  
  : , : , :
375instantiation599, 429  ⊢  
  : , : , :
376instantiation711, 595, 430,  ⊢  
  : , :
377instantiation704  ⊢  
  : , :
378instantiation749, 511, 431  ⊢  
  : , : , :
379instantiation696, 432, 433  ⊢  
  : , : , :
380instantiation704  ⊢  
  : , :
381instantiation704  ⊢  
  : , :
382conjecture  ⊢  
 proveit.numbers.number_sets.integers.zero_set_within_int
383conjecture  ⊢  
 proveit.core_expr_types.tuples.range_len_is_nat
384instantiation670, 507, 434  ⊢  
  : , : , :
385instantiation599, 600  ⊢  
  : , : , :
386instantiation601, 435, 436, 437  ⊢  
  : , : , : , :
387instantiation620, 542, 716, 678, 621, 438*, 514*  ⊢  
  : , : , :
388conjecture  ⊢  
 proveit.numbers.addition.add_nat_closure_bin
389instantiation749, 511, 439  ⊢  
  : , : , :
390instantiation657, 440, 441  ⊢  
  : , : , :
391instantiation657, 442, 443  ⊢  
  : , : , :
392instantiation643, 689, 736, 748, 690, 616, 619, 649, 662,  ⊢  
  : , : , : , : , : , :
393conjecture  ⊢  
 proveit.core_expr_types.tuples.shift_equivalence
394instantiation444, 445, 446  ⊢  
  :
395instantiation611, 447  ⊢  
  : , :
396instantiation611, 448  ⊢  
  : , :
397instantiation449, 744, 746  ⊢  
  : , : , : , : , :
398generalization450  ⊢  
399instantiation599, 453  ⊢  
  : , : , :
400instantiation657, 451, 452  ⊢  
  : , : , :
401instantiation599, 453  ⊢  
  : , : , :
402instantiation749, 731, 454,  ⊢  
  : , : , :
403conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_lower_bound
404instantiation615, 748, 689, 690, 649, 682, 662, 617  ⊢  
  : , : , : , : , : , : , : , :
405instantiation704  ⊢  
  : , :
406instantiation643, 689, 674, 748, 690, 455, 677, 646, 662, 682,  ⊢  
  : , : , : , : , : , :
407instantiation614, 748, 689, 690, 677, 682, 662,  ⊢  
  : , : , : , : , : , : , : , :
408instantiation749, 725, 456,  ⊢  
  : , : , :
409theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
410instantiation457, 736, 458, 459, 460, 530  ⊢  
  : , : , : , :
411instantiation657, 461, 462  ⊢  
  : , : , :
412instantiation464, 465  ⊢  
  : , : , :
413conjecture  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
414instantiation749, 511, 463  ⊢  
  : , : , :
415instantiation464, 465  ⊢  
  : , : , :
416instantiation657, 466, 467  ⊢  
  : , : , :
417instantiation468, 469  ⊢  
  : , :
418conjecture  ⊢  
 proveit.logic.booleans.conjunction.conjunction_from_quantification
419instantiation620, 542, 715, 678, 536, 470*, 471*  ⊢  
  : , : , :
420instantiation557, 558, 472, 473,  ⊢  
  : , : , : , :
421conjecture  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
422instantiation615, 748, 689, 690, 649, 712, 662, 577  ⊢  
  : , : , : , : , : , : , : , :
423instantiation474, 662, 651  ⊢  
  : , :
424instantiation749, 728, 475  ⊢  
  : , : , :
425instantiation704  ⊢  
  : , :
426conjecture  ⊢  
 proveit.numbers.addition.elim_zero_right
427instantiation701, 673, 476  ⊢  
  : , :
428instantiation657, 477, 478  ⊢  
  : , : , :
429instantiation599, 539  ⊢  
  : , : , :
430instantiation670, 479, 480,  ⊢  
  : , : , :
431instantiation571, 751, 652  ⊢  
  : , :
432instantiation708, 481  ⊢  
  : , :
433instantiation482, 483  ⊢  
  : , :
434instantiation601, 539, 484, 485  ⊢  
  : , : , : , :
435instantiation643, 748, 736, 633, 634, 662, 683, 712  ⊢  
  : , : , : , : , : , :
436instantiation635, 689, 674, 690, 486, 662, 683, 712  ⊢  
  : , : , : , :
437instantiation618, 712, 662, 577  ⊢  
  : , : , :
438instantiation601, 487, 488, 489  ⊢  
  : , : , : , :
439instantiation490, 748, 689, 690, 491  ⊢  
  : , : , : , : , :
440instantiation599, 632  ⊢  
  : , : , :
441instantiation657, 492, 493  ⊢  
  : , : , :
442instantiation599, 632  ⊢  
  : , : , :
443instantiation590, 662  ⊢  
  :
444conjecture  ⊢  
 proveit.numbers.number_sets.integers.nonneg_int_is_natural
445instantiation742, 494, 495  ⊢  
  : , :
446instantiation496, 497  ⊢  
  : , :
447instantiation657, 498, 499  ⊢  
  : , : , :
448instantiation581, 662, 500, 682, 514  ⊢  
  : , : , :
449conjecture  ⊢  
 proveit.core_expr_types.tuples.range_fn_transformation
450instantiation657, 501, 502,  ⊢  
  : , : , :
451instantiation643, 689, 736, 748, 690, 589, 649, 682  ⊢  
  : , : , : , : , : , :
452instantiation637, 748, 736, 689, 606, 690, 649, 682, 680*  ⊢  
  : , : , : , : , : , :
453instantiation661, 682  ⊢  
  :
454instantiation749, 734, 503,  ⊢  
  : , : , :
455instantiation694  ⊢  
  : , : , :
456assumption  ⊢  
457axiom  ⊢  
 proveit.core_expr_types.operations.operands_substitution
458instantiation704  ⊢  
  : , :
459instantiation704  ⊢  
  : , :
460instantiation641, 682, 617  ⊢  
  : , : , :
461instantiation643, 748, 736, 689, 645, 690, 682, 662, 646  ⊢  
  : , : , : , : , : , :
462instantiation504, 682, 662, 617  ⊢  
  : , : , :
463axiom  ⊢  
 proveit.physics.quantum.QPE._s_in_nat_pos
464conjecture  ⊢  
 proveit.core_expr_types.tuples.range_len
465instantiation505, 674, 506, 689, 507, 748  ⊢  
  : , :
466instantiation599, 539  ⊢  
  : , : , :
467instantiation601, 508, 509, 510  ⊢  
  : , : , : , :
468conjecture  ⊢  
 proveit.core_expr_types.tuples.range_from1_len
469instantiation749, 511, 751  ⊢  
  : , : , :
470instantiation657, 512, 513  ⊢  
  : , : , :
471instantiation601, 514, 617, 515  ⊢  
  : , : , : , :
472instantiation516, 682, 517, 518  ⊢  
  : , :
473instantiation519, 558, 520, 521,  ⊢  
  : , : , : , :
474conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_reverse
475instantiation522, 678, 523  ⊢  
  : , :
476instantiation670, 524, 525  ⊢  
  : , : , :
477instantiation688, 748, 674, 689, 526, 690, 673, 702, 597, 692  ⊢  
  : , : , : , : , : , :
478instantiation688, 689, 736, 674, 690, 675, 526, 712, 693, 702, 597, 692  ⊢  
  : , : , : , : , : , :
479instantiation701, 673, 527,  ⊢  
  : , :
480instantiation657, 528, 529,  ⊢  
  : , : , :
481conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_set_within_nat
482conjecture  ⊢  
 proveit.logic.sets.enumeration.fold_singleton
483conjecture  ⊢  
 proveit.numbers.negation.negated_zero
484instantiation669  ⊢  
  :
485instantiation611, 530  ⊢  
  : , :
486instantiation694  ⊢  
  : , : , :
487instantiation657, 531, 532  ⊢  
  : , : , :
488instantiation581, 607, 662, 712, 533  ⊢  
  : , : , :
489instantiation669  ⊢  
  :
490conjecture  ⊢  
 proveit.numbers.addition.add_nat_pos_from_nonneg
491conjecture  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
492instantiation643, 689, 736, 748, 690, 589, 649, 682, 662  ⊢  
  : , : , : , : , : , :
493instantiation534, 662, 682, 651  ⊢  
  : , : , :
494instantiation749, 750, 535  ⊢  
  : , : , :
495instantiation745, 730  ⊢  
  :
496conjecture  ⊢  
 proveit.numbers.addition.subtraction.nonneg_difference
497instantiation620, 640, 715, 678, 536, 537*, 538*  ⊢  
  : , : , :
498instantiation599, 539  ⊢  
  : , : , :
499instantiation657, 540, 541  ⊢  
  : , : , :
500instantiation749, 728, 542  ⊢  
  : , : , :
501instantiation599, 543,  ⊢  
  : , : , :
502instantiation657, 544, 545,  ⊢  
  : , : , :
503instantiation749, 546, 547,  ⊢  
  : , : , :
504conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_13
505conjecture  ⊢  
 proveit.numbers.addition.add_nat_closure
506instantiation694  ⊢  
  : , : , :
507instantiation548, 549  ⊢  
  :
508instantiation643, 748, 736, 645, 634, 662, 646, 682  ⊢  
  : , : , : , : , : , :
509instantiation635, 689, 674, 690, 550, 662, 646, 682  ⊢  
  : , : , : , :
510instantiation618, 682, 662, 617  ⊢  
  : , : , :
511conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
512instantiation643, 748, 736, 689, 589, 690, 634, 649, 682  ⊢  
  : , : , : , : , : , :
513instantiation635, 689, 736, 690, 589, 649, 682  ⊢  
  : , : , : , :
514instantiation657, 551, 552  ⊢  
  : , : , :
515instantiation611, 553  ⊢  
  : , :
516conjecture  ⊢  
 proveit.numbers.division.div_complex_closure
517instantiation554, 712  ⊢  
  :
518instantiation555, 593, 556  ⊢  
  : , :
519conjecture  ⊢  
 proveit.linear_algebra.addition.binary_closure
520conjecture  ⊢  
 proveit.physics.quantum.algebra.ket_zero_in_qubit_space
521instantiation557, 558, 559, 560,  ⊢  
  : , : , : , :
522conjecture  ⊢  
 proveit.numbers.addition.add_real_closure_bin
523instantiation561, 721  ⊢  
  :
524instantiation701, 562, 692  ⊢  
  : , :
525instantiation688, 689, 736, 748, 690, 563, 702, 597, 692  ⊢  
  : , : , : , : , : , :
526instantiation694  ⊢  
  : , : , :
527instantiation670, 564, 565,  ⊢  
  : , : , :
528instantiation688, 748, 674, 689, 676, 690, 673, 702, 630, 692,  ⊢  
  : , : , : , : , : , :
529instantiation688, 689, 736, 674, 690, 675, 676, 712, 693, 702, 630, 692,  ⊢  
  : , : , : , : , : , :
530instantiation657, 566, 567  ⊢  
  : , : , :
531instantiation643, 748, 736, 689, 589, 690, 682, 649  ⊢  
  : , : , : , : , : , :
532instantiation657, 568, 569  ⊢  
  : , : , :
533instantiation670, 576, 570  ⊢  
  : , : , :
534conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_31
535instantiation571, 652  ⊢  
  : , :
536instantiation572, 573  ⊢  
  : , :
537instantiation657, 574, 575  ⊢  
  : , : , :
538instantiation601, 576, 577, 578  ⊢  
  : , : , : , :
539instantiation631, 649, 682, 632*  ⊢  
  : , :
540instantiation657, 579, 580  ⊢  
  : , : , :
541instantiation581, 682, 712, 680  ⊢  
  : , : , :
542instantiation749, 731, 582  ⊢  
  : , : , :
543instantiation643, 748, 736, 689, 589, 690, 619, 649, 682,  ⊢  
  : , : , : , : , : , :
544instantiation643, 689, 674, 736, 690, 583, 584, 619, 649, 682, 646, 662,  ⊢  
  : , : , : , : , : , :
545instantiation657, 585, 586,  ⊢  
  : , : , :
546instantiation739, 730, 744  ⊢  
  : , :
547assumption  ⊢  
548conjecture  ⊢  
 proveit.numbers.negation.nat_closure
549instantiation587, 740, 588  ⊢  
  :
550instantiation694  ⊢  
  : , : , :
551instantiation643, 748, 736, 689, 589, 690, 662, 649, 682  ⊢  
  : , : , : , : , : , :
552instantiation641, 662, 682, 651  ⊢  
  : , : , :
553instantiation590, 682  ⊢  
  :
554conjecture  ⊢  
 proveit.numbers.exponentiation.sqrt_complex_closure
555conjecture  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
556instantiation591, 592, 593  ⊢  
  : , :
557conjecture  ⊢  
 proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
558instantiation594, 654  ⊢  
  :
559instantiation711, 595, 596,  ⊢  
  : , :
560conjecture  ⊢  
 proveit.physics.quantum.algebra.ket_one_in_qubit_space
561conjecture  ⊢  
 proveit.numbers.negation.real_closure
562instantiation701, 702, 597  ⊢  
  : , :
563instantiation704  ⊢  
  : , :
564instantiation701, 598, 692,  ⊢  
  : , :
565instantiation688, 689, 736, 748, 690, 691, 702, 630, 692,  ⊢  
  : , : , : , : , : , :
566instantiation599, 600  ⊢  
  : , : , :
567instantiation601, 602, 603, 604  ⊢  
  : , : , : , :
568instantiation605, 748, 689, 690, 682, 649  ⊢  
  : , : , : , : , : , : , :
569instantiation637, 689, 736, 748, 690, 606, 682, 649, 680*  ⊢  
  : , : , : , : , : , :
570instantiation681, 662, 607  ⊢  
  : , :
571conjecture  ⊢  
 proveit.numbers.addition.add_nat_pos_closure_bin
572conjecture  ⊢  
 proveit.numbers.ordering.relax_less
573instantiation608, 751  ⊢  
  :
574instantiation643, 748, 736, 689, 644, 690, 634, 649, 712  ⊢  
  : , : , : , : , : , :
575instantiation635, 689, 736, 690, 644, 649, 712  ⊢  
  : , : , : , :
576instantiation657, 609, 610  ⊢  
  : , : , :
577instantiation669  ⊢  
  :
578instantiation611, 680  ⊢  
  : , :
579instantiation657, 612, 613  ⊢  
  : , : , :
580instantiation614, 689, 748, 690, 662, 712, 646  ⊢  
  : , : , : , : , : , : , : , :
581conjecture  ⊢  
 proveit.numbers.addition.subtraction.subtract_from_add
582instantiation749, 734, 740  ⊢  
  : , : , :
583instantiation694  ⊢  
  : , : , :
584instantiation704  ⊢  
  : , :
585instantiation615, 736, 689, 748, 616, 690, 619, 649, 682, 662, 617,  ⊢  
  : , : , : , : , : , : , : , :
586instantiation618, 662, 619, 651,  ⊢  
  : , : , :
587conjecture  ⊢  
 proveit.numbers.number_sets.integers.nonpos_int_is_int_nonpos
588instantiation620, 668, 716, 678, 621, 622*, 623*  ⊢  
  : , : , :
589instantiation704  ⊢  
  : , :
590conjecture  ⊢  
 proveit.numbers.addition.elim_zero_left
591conjecture  ⊢  
 proveit.numbers.division.div_rational_nonzero_closure
592instantiation749, 625, 624  ⊢  
  : , : , :
593instantiation749, 625, 626  ⊢  
  : , : , :
594conjecture  ⊢  
 proveit.linear_algebra.complex_vec_set_is_vec_space
595instantiation749, 728, 627  ⊢  
  : , : , :
596instantiation670, 628, 629,  ⊢  
  : , : , :
597instantiation711, 712, 642  ⊢  
  : , :
598instantiation701, 702, 630,  ⊢  
  : , :
599axiom  ⊢  
 proveit.logic.equality.substitution
600instantiation631, 649, 712, 632*  ⊢  
  : , :
601conjecture  ⊢  
 proveit.logic.equality.four_chain_transitivity
602instantiation643, 748, 736, 633, 634, 662, 683, 682  ⊢  
  : , : , : , : , : , :
603instantiation635, 689, 674, 690, 636, 662, 683, 682  ⊢  
  : , : , : , :
604instantiation637, 748, 736, 689, 638, 690, 662, 683, 682, 639*  ⊢  
  : , : , : , : , : , :
605conjecture  ⊢  
 proveit.numbers.addition.leftward_commutation
606instantiation704  ⊢  
  : , :
607instantiation749, 728, 640  ⊢  
  : , : , :
608conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
609instantiation643, 748, 736, 689, 644, 690, 662, 649, 712  ⊢  
  : , : , : , : , : , :
610instantiation641, 662, 712, 651  ⊢  
  : , : , :
611theorem  ⊢  
 proveit.logic.equality.equals_reversal
612instantiation643, 689, 736, 748, 690, 644, 649, 712, 642  ⊢  
  : , : , : , : , : , :
613instantiation643, 736, 689, 644, 645, 690, 649, 712, 662, 646  ⊢  
  : , : , : , : , : , :
614conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_general_rev
615conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_general
616instantiation704  ⊢  
  : , :
617instantiation669  ⊢  
  :
618conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_32
619instantiation749, 728, 647,  ⊢  
  : , : , :
620conjecture  ⊢  
 proveit.numbers.addition.weak_bound_via_left_term_bound
621instantiation648, 751  ⊢  
  :
622instantiation681, 682, 649  ⊢  
  : , :
623instantiation650, 662, 651  ⊢  
  : , :
624instantiation749, 653, 652  ⊢  
  : , : , :
625conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
626instantiation749, 653, 654  ⊢  
  : , : , :
627instantiation749, 718, 655  ⊢  
  : , : , :
628instantiation701, 673, 656,  ⊢  
  : , :
629instantiation657, 658, 659,  ⊢  
  : , : , :
630instantiation711, 712, 660,  ⊢  
  : , :
631conjecture  ⊢  
 proveit.numbers.negation.distribute_neg_through_binary_sum
632instantiation661, 662  ⊢  
  :
633instantiation704  ⊢  
  : , :
634conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.zero_is_complex
635conjecture  ⊢  
 proveit.numbers.addition.elim_zero_any
636instantiation694  ⊢  
  : , : , :
637conjecture  ⊢  
 proveit.numbers.addition.association
638instantiation704  ⊢  
  : , :
639instantiation670, 663, 664  ⊢  
  : , : , :
640instantiation749, 731, 665  ⊢  
  : , : , :
641conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_12
642instantiation749, 728, 666  ⊢  
  : , : , :
643conjecture  ⊢  
 proveit.numbers.addition.disassociation
644instantiation704  ⊢  
  : , :
645instantiation704  ⊢  
  : , :
646instantiation722, 682  ⊢  
  :
647instantiation749, 731, 667,  ⊢  
  : , : , :
648conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
649instantiation749, 728, 668  ⊢  
  : , : , :
650conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_basic
651instantiation669  ⊢  
  :
652conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat1
653conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
654conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat2
655conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.e_is_real_pos
656instantiation670, 671, 672,  ⊢  
  : , : , :
657axiom  ⊢  
 proveit.logic.equality.equals_transitivity
658instantiation688, 748, 674, 689, 676, 690, 673, 702, 703, 692,  ⊢  
  : , : , : , : , : , :
659instantiation688, 689, 736, 674, 690, 675, 676, 712, 693, 702, 703, 692,  ⊢  
  : , : , : , : , : , :
660instantiation722, 677,  ⊢  
  :
661conjecture  ⊢  
 proveit.numbers.negation.double_negation
662instantiation749, 728, 678  ⊢  
  : , : , :
663instantiation679, 682, 712, 680  ⊢  
  : , : , :
664instantiation681, 682, 683  ⊢  
  : , :
665instantiation749, 734, 730  ⊢  
  : , : , :
666instantiation749, 731, 684  ⊢  
  : , : , :
667instantiation749, 734, 685,  ⊢  
  : , : , :
668instantiation749, 731, 686  ⊢  
  : , : , :
669axiom  ⊢  
 proveit.logic.equality.equals_reflexivity
670theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
671instantiation701, 687, 692,  ⊢  
  : , :
672instantiation688, 689, 736, 748, 690, 691, 702, 703, 692,  ⊢  
  : , : , : , : , : , :
673instantiation701, 712, 693  ⊢  
  : , :
674conjecture  ⊢  
 proveit.numbers.numerals.decimals.nat3
675instantiation704  ⊢  
  : , :
676instantiation694  ⊢  
  : , : , :
677instantiation749, 728, 695,  ⊢  
  : , : , :
678instantiation696, 697, 751  ⊢  
  : , : , :
679conjecture  ⊢  
 proveit.numbers.addition.subtraction.subtract_from_add_reversed
680conjecture  ⊢  
 proveit.numbers.numerals.decimals.add_1_1
681conjecture  ⊢  
 proveit.numbers.addition.commutation
682instantiation749, 728, 716  ⊢  
  : , : , :
683instantiation722, 712  ⊢  
  :
684instantiation749, 734, 698  ⊢  
  : , : , :
685instantiation749, 699, 700,  ⊢  
  : , : , :
686instantiation749, 734, 743  ⊢  
  : , : , :
687instantiation701, 702, 703,  ⊢  
  : , :
688conjecture  ⊢  
 proveit.numbers.multiplication.disassociation
689axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
690conjecture  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
691instantiation704  ⊢  
  : , :
692instantiation749, 728, 705  ⊢  
  : , : , :
693instantiation749, 728, 706  ⊢  
  : , : , :
694conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
695instantiation749, 731, 707,  ⊢  
  : , : , :
696theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
697instantiation708, 709  ⊢  
  : , :
698instantiation742, 746, 710  ⊢  
  : , :
699instantiation739, 744, 746  ⊢  
  : , :
700assumption  ⊢  
701conjecture  ⊢  
 proveit.numbers.multiplication.mult_complex_closure_bin
702conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.i_is_complex
703instantiation711, 712, 713,  ⊢  
  : , :
704conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
705instantiation714, 715, 716, 717  ⊢  
  : , : , :
706instantiation749, 718, 719  ⊢  
  : , : , :
707instantiation749, 734, 720,  ⊢  
  : , : , :
708theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
709conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
710instantiation745, 744  ⊢  
  :
711conjecture  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
712instantiation749, 728, 721  ⊢  
  : , : , :
713instantiation722, 723,  ⊢  
  :
714conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
715conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
716instantiation749, 731, 724  ⊢  
  : , : , :
717axiom  ⊢  
 proveit.physics.quantum.QPE._phase_in_interval
718conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real
719conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.pi_is_real_pos
720instantiation749, 725, 726,  ⊢  
  : , : , :
721instantiation749, 731, 727  ⊢  
  : , : , :
722conjecture  ⊢  
 proveit.numbers.negation.complex_closure
723instantiation749, 728, 729,  ⊢  
  : , : , :
724instantiation749, 734, 744  ⊢  
  : , : , :
725instantiation739, 730, 741  ⊢  
  : , :
726assumption  ⊢  
727instantiation749, 734, 733  ⊢  
  : , : , :
728conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
729instantiation749, 731, 732,  ⊢  
  : , : , :
730instantiation742, 743, 733  ⊢  
  : , :
731conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
732instantiation749, 734, 735,  ⊢  
  : , : , :
733instantiation749, 747, 736  ⊢  
  : , : , :
734conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
735instantiation749, 737, 738,  ⊢  
  : , : , :
736theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
737instantiation739, 740, 741  ⊢  
  : , :
738assumption  ⊢  
739conjecture  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
740instantiation742, 743, 744  ⊢  
  : , :
741conjecture  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
742conjecture  ⊢  
 proveit.numbers.addition.add_int_closure_bin
743instantiation745, 746  ⊢  
  :
744instantiation749, 747, 748  ⊢  
  : , : , :
745conjecture  ⊢  
 proveit.numbers.negation.int_closure
746instantiation749, 750, 751  ⊢  
  : , : , :
747conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
748theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
749theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
750conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
751assumption  ⊢  
*equality replacement requirements